T, A:Type, a, x:Id, f:(AT), tg:Id, l:IdLnk, es:ES.
locl(a) sends [tg,f{AT}(x)] on link l once  Prop 

latex

Definitions	Type, t  T, Id, x:AB(x), IdLnk, ES, x:A. B(x), E, s = t, locl(a), left+right, Knd, x:AB(x), P & Q, A & B, {T}, P  Q, sender(e), A/x,y. B(x;y), 1of(t), kind(e), vartype(i;x), b, x when e, f(a), valtype(e), val(e), rcv(l,tg), x:A. B(x), source(l), Prop, locl(a) sends [tg,f{AT}(x)] on link l once
Lemmas	lsrc wf, es-valtype wf, rcv wf, es-val wf, subtype rel self, es-when wf, es-vartype wf, Knd wf, es-kind wf, es-sender wf, es-kind-rcv, locl wf, es-E wf, event system wf, IdLnk wf, Id wf